T:Type, x:T, a:Atom1. AtomFree(Type;T)  AtomFree(T;x)  x:T>>a  False 

latex

Definitions	False, P  Q, A, x:AB(x), x:A. B(x), x:T>>a, Type, t  T, Atom$n, x:A. B(x), AtomFree(T;x), Void
Lemmas	inheres wf, atom-free wf